k:Knd, T, A, B:Type, l:IdLnk, x, tg:Id, f:(ABT), c:(AB), es:ES.
sends1-p(es;x;A;k;B;l;tg;T;a,b. if c(a,b) then [(f(a,b))] else [] fi )
  k(v:B) sends
  kf(x:A,v) on
  kl tagged with tg:T
  kprovided c(x,v) 

latex

Definitions

False, A, A  B, Y, ||as||, i  j , hd(l), P  Q, P  Q, x:A. B(x), Top, ff, True, tt, , t  T, b, P & Q, A c B,  k(v:B) sends f(x:A,v) on l tagged with tg:T provided c(x,v), if b then t else f fi , P  Q, IdLnk, Knd, x:A. B(x), P  Q, Dec(P), {T}, map(f;as), Unit, , sends1-p(es;x;A;k;B;l;tg;T;f),

Lemmas

nil member, decidable false, l member wf, ge wf, hd wf, es-kind-rcv, member singleton, es-sender wf, rcv wf, non neg length, length-map, length wf1, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, false wf, bnot wf, assert wf, map wf, not wf, true wf, es-val wf, es-vartype wf, es-when wf, IdLnk wf, Id wf, bool wf, event system wf, ifthenelse wf, sends1-p wf, es-E wf, lsrc wf, es-loc wf, es-kind wf, Knd wf